Inference at * 2 1 
Iof proof for Lemma member nth tl:



1. T : Type
2. n : 
3. 0 < n
4. x:T, L:(T List). (x  nth_tl(n - 1;L))  (x  L)
5. x : T
6. T List
  (x  nth_tl(n;[]))  (x  []) 

latex

 by ((Subst' nth_tl(n;[]) = [] ( 0)) 
CollapseTHEN (Auto)) 

latex

C1: .....equality..... NILNIL

C1:   nth_tl(n;[]) = []
C.

Definitions	s = t, type List, nth_tl(n;as), [], A List, , S  T, Top, x:A.B(x), Void, ||as||, i  j , A  B, P  Q, P  Q, P & Q, x:A  B(x), [car / cdr], SQType(T), {T}, s ~ t, n - m, #$n, a < b, , Type, P  Q, , (x  l), x:A. B(x), x:AB(x), t  T
Lemmas	length wf nat, member wf, top wf, non neg length, cons one one, guard wf, l member wf